Nuprl Lemma : test-spec-feasible
0,22
postcript
pdf
R-Feasible{i:l}
R-Feasible
(es-realizer(TERMOF{
test-spec
:ObjectId,
R-Feasible(es-realizer(TERMOF{
done:ut2,
R-Feasible(es-realizer(TERMOF{
tg:ut2,
R-Feasible(es-realizer(TERMOF{
b:ut2,
R-Feasible(es-realizer(TERMOF{
done1:ut2,
R-Feasible(es-realizer(TERMOF{
1:ut2,
R-Feasible(es-realizer(TERMOF{
loc2:ut2,
R-Feasible(es-realizer(TERMOF{
loc1:ut2,
R-Feasible(es-realizer(TERMOF{
\\v:l,
R-Feasible(es-realizer(TERMOF{
i:l}))
latex
Definitions
,
Type
,
AtomFree(
T
;
x
)
,
A
&
B
,
P
&
Q
,
Normal(
T
)
,
t
T
,
"$x"
,
Id
,
<
a
,
b
>
,
lnk$n{$a to $b}
,
IdLnk
,
x
.
A
(
x
)
,
P
Q
,
x
:
A
.
B
(
x
)
,
implies-es-real
,
f
(
a
)
,
send-once-realizable
,
test-spec
,
es-realizer(
p
)
Lemmas
send
onceR
feasible
,
bool-inhabited
,
bool
wf
origin
, Type, AtomFree(T;x), A & B, P & Q, Normal(T), t 
T, "$x", Id, <a,b>, lnk$n{$a to $b}, IdLnk, 
x.A(x), P 
Q, 
x:A. B(x), implies-es-real, f(a), send-once-realizable, test-spec, es-realizer(p)